Step of Proof: bool-to-dcdr_wf
11,40
postcript
pdf
Inference at
*
1
2
I
of proof for Lemma
bool-to-dcdr
wf
:
1.
A
: Type
2.
f
:
A
3.
x
:
A
4. {
f
}
(
x
:
A
. Dec(
f
(
x
) = tt))
{
f
}
(
x
)
Dec(
f
(
x
) = tt)
latex
by Auto
latex
.
Definitions
f
(
a
)
,
{
f
}
,
t
T
origin
(
x:A. Dec(f(x) = tt))
{f}(x) Dec(f(x) = tt)
by Auto
.
(x:A. Dec(f(x) = tt))
{f}(x) Dec(f(x) = tt)
by Auto
. T